Nuprl Lemma : rng_times_nat_op
6,26
postcript
pdf
r
:Rng,
a
,
b
:|
r
|,
n
:
. (
a
* (
n
r
b
)) = (
n
r
(
a
*
b
))
|
r
|
latex
Definitions
x
:
A
.
B
(
x
)
,
n
r
e
,
n
e
,
n
x(
op
;
id
)
e
,
t
T
,
P
Q
,
A
B
,
A
,
False
,
x
.
t
(
x
)
,
Rng
,
,
x
(
s
)
,
lb
i
<
ub
.
E
(
i
)
,
(
r
)
i
k
<
j
.
E
(
k
)
Lemmas
nat
wf
,
rng
car
wf
,
rng
wf
,
rng
times
sum
l
,
int
seg
wf
origin
r:Rng, a, b:|r|, n:
. (a * (n 
r b)) = (n r (a * b)) 
|r| r:Rng, a, b:|r|, n:. (a * (n r b)) = (n r (a * b)) |r| x:A. B(x)r e e T
Q
B
A
x. t(x)
lb i < ub. E(i)
(r) i k < j. E(k)